After spending two full days (mostly on recompiling stuff), I managed to adapt Analysis to math-comp/math-comp#1125. Most issues have been fixed on the MathComp side. However, it seems that I happened to break the mechanism to automatically prove positivity conditions like 0 < _ / _, and I couldn't find where it is implemented (couldn't find mulr_gt0 declared as a hint, for example).

However, it seems that I happened to break the mechanism to automatically prove positivity conditions like 0 < _ / _, and I couldn't find where it is implemented (couldn't find mulr_gt0 declared as a hint, for example).

Isn't it the mechanism implemented in signed.v? @proux01

Yes, that's in thories/signed.v

I'm taking a look at signed.v. The positivity, negativity, nullity, etc. specification of functions are expressed by the following datatypes there:

Variant nullity := NonZero | MaybeZero.

Variant sign := EqZero | NonNeg | NonPos.
Variant real := Sign of sign | AnySign.
Variant reality := Real of real | Arbitrary.

I have the impression that it should be expressed as a tuple of 4 boolean values bool * bool * bool * bool, whose elements express the possibility of the value being negative, zero, positive, and non-real. Then, the arbitrary real value would be (true, true, true, false), and arbitrary non-zero value would be (true, false, true, true).

Also, the instance for normr doesn't seem to be strong enough to prove 0 < normr x for arbitrary non-zero value x.

I have the impression that it should be expressed as a tuple of 4 boolean values bool * bool * bool * bool, whose elements express the possibility of the value being negative, zero, positive, and non-real. Then, the arbitrary real value would be (true, true, true, false), and arbitrary non-zero value would be (true, false, true, true).

Sorry, could you explain what would be the advantages of such an encoding? I can clearly see the drawback of having all parameters of the same type (much higher risk to inadvertently mixing them) but not the advantages.

Also, the instance for normr doesn't seem to be strong enough to prove 0 < normr x for arbitrary non-zero value x.

Sure, feel free to strengthen it. The only thing proved is the soundness, not that we provide the best approximation.

Sorry, could you explain what would be the advantages of such an encoding? I can clearly see the drawback of having all parameters of the same type (much higher risk to inadvertently mixing them) but not the advantages.

The current encoding doesn't seem to allow us to encode some cases, e.g., x such that (0 < x) || (x \notin Rreal). Also, there seems to be an overlap between what nullity and sign mean, e.g., I don't get what the combination of NonZero and EqZero would mean.

bool * bool * bool * bool can be replaced with the tuple of the following four types.

Variant positivity := NonPos | MaybePos.
Variant nullity := NonZero | MaybeZero.
Variant negativity := NonNeg | MaybeNeg.
Variant reality := IsReal | MaybeNonReal.

The current encoding doesn't seem to allow us to encode some cases, e.g., x such that (0 < x) || (x \notin Rreal).

Right, that's the point of an abstraction to not be able to encode precisely everything. And indeed it could be refined if needed (but there will always be things that cannot be encoded).

I don't get what the combination of NonZero and EqZero would mean.

That's the set of values that are both non zero and equal to zero, that is the empty set (enabling to prove False).

bool * bool * bool * bool can be replaced with the tuple of the following four types.

Sure, precise types are better than boolean, but I still fail to see the details. What would be the semantics of a tuple? I would expect conjunction of individual semantics of each element, but then some encoding become uselessly redundant: for instance NonPos * MaybeReal and NonPos * IsReal represent the same thing since being NonPos implies being Real.

For instance NonPos * MaybeReal and NonPos * IsReal represent the same thing since being NonPos implies being Real.

NonPos means x in question satisfies ~~ (0 < x), which includes the case that x is not real. (NonPos doesn't imply being real here.)

Ha, my bad, I thought it was the usual mathematical definition x <= 0. Then indeed you're probably right. Beware however that adapting all of signed.v might require quite some work.

Since we decided to remove the new parameters of the Semilinear structure (and rename it back to Linear, see math-comp/math-comp#1125 (comment)), we no longer need this overlay PR. I'm closing it.